// ApplicationTerm.cpp : implementation file
//

#include "stdafx.h"
#include "ApplicationTerm.h"
Token::const_reference ApplicationTerm::getRight() const {
	return LeftRight.getRight();
	};


Term::const_reference ApplicationTerm::getLeft() const	 {
	return _TERM(LeftRight.getLeft());
	};

Token::pointer ApplicationTerm::normalized() const{
	string DebugLeft = getLeft().view();
	string DebugRight = getRight().view();

	if((getRight().isType())&&(getLeft().isAbstractTypeTerm())){
				Token::pointer NewLeft = getLeft().normalized();
				Token::pointer ArgTy= getRight().normalized();
				Token::pointer Temp = NewLeft->applyArgument(*ArgTy);
				delete NewLeft;		
				delete  ArgTy;
				Token::pointer Res = Temp->normalized();
				delete Temp;
				return Res;
		}
	
	if(getRight().isTerm()){
				Token::pointer NewLeft = getLeft().normalized();
				Token::pointer NewRight = getRight().normalized();
				if(_TERM(*NewLeft).isAbstractTerm()){
					Token::pointer Temp = NewLeft->applyArgument(*NewRight);
					delete NewLeft;
					delete NewRight;
					Token::pointer Res = Temp->normalized();
					delete Temp;
					return Res;
					}
				else{
					   Token::pointer Res = new ApplicationTerm(_TERM(*NewLeft),*NewRight);
					   delete NewLeft;
						delete NewRight;
							return Res;
					}
		}

		return this->clone();
		//throw Term::exception("Unexpected term/type pair at  Term::pointer ApplicationTerm::normalized() const");
}

Token::pointer ApplicationTerm::applyArgument(Token::const_reference)  const{
	throw Term::exception("Token::pointer ApplicationTerm::applyArgument(Token::const_reference)  const Not Implemented");
}
Token::pointer ApplicationTerm::clone() const{
      return new ApplicationTerm(*this);
}


bool ApplicationTerm::isReducible() const {
	if(isRedex()) return true;
	if(getLeft().isReducible()) return true;
	if(getRight().isReducible()) return true;
	return false;
}
bool ApplicationTerm::isRedex() const{
		if(getRight().isTerm())
			return getLeft().isAbstractTerm();
		else
			return getLeft().isAbstractTypeTerm();
}
string ApplicationTerm::toString() const{

		return getLeft().toString() + string("(")
					+ getRight().toString() + string(")");
	
}

string ApplicationTerm::view() const{
	return string("[[")+
		getLeft().view() + string("][") + 
		getRight().view() + string("]]") + 
		string(":")+getType().view();
}

bool ApplicationTerm::operator==(Token::const_reference To)const{
	if(To.isTerm())
		if(_TERM(To).isApplicationTerm())
			return(LeftRight==(_APPLICATIONTERM(To)).LeftRight);

	return false;
}
Token::pointer ApplicationTerm::replaceAll(Token::const_reference To1, Token::const_reference To2) const{
	TokenPair* NewPair = LeftRight.replaceAll(To1, To2);
	ApplicationTerm* AppPtr = new ApplicationTerm(*this);
	AppPtr->LeftRight = *NewPair;
	delete NewPair;
	return AppPtr;
}





bool ApplicationTerm::TypeOccursinFreeVariable(Type::const_reference Ty) const {
	if(getLeft().TypeOccursinFreeVariable(Ty)) return true;
	if(getRight().isTerm()) return _TERM(getRight()).TypeOccursinFreeVariable(Ty);
	return false;
	}







ApplicationTerm::ApplicationTerm(Term::const_reference TL, Token::const_reference TR, const string& ss):
	Term(TL.getType( )), LeftRight(TL,TR)
{
   try{
	   Type::pointer Ty;
	   if(TR.isType())
		   Ty =  Term::ResolveType(TL.getType( ), _TYPE(TR));
	   else
		   Ty = Term::ResolveType(TL.getType( ), _TERM(TR).getType( ));

	   this->assignType(*Ty);
	   delete Ty;

       }
   catch(Term::exception err){
       throw err;
    }
}

ApplicationTerm::ApplicationTerm(const ApplicationTerm& Ter):
Term(Ter),LeftRight(Ter.LeftRight){}
ApplicationTerm::~ApplicationTerm(){}

Token::const_reference InvertedListTerm::getRight() const {
	return *Applications[Applications.size()-1];
	};

InvertedListTerm::InvertedListTerm(vector<Token*> TV, const string& ss):
	Term(ss), Applications(TV){		
		try{
			if(TV[0]->isTerm( )){		
				Type::pointer TyOld = static_cast<Type::pointer>(_TERM(*TV[0]).getType( ).clone( ));
				Type::pointer Ty;
				for(size_t i=1; i<TV.size( ); i++)	{
					if(TV[i]->isType())
						Ty = Term::ResolveType(*TyOld, _TYPE(*TV[i]));
					else
						Ty = Term::ResolveType(*TyOld, _TERM(*TV[i]).getType( ));	
					delete TyOld;
					TyOld = Ty;
					}
			this->assignType(*TyOld);
			delete TyOld;
			return;
				}
			}
	catch(Token::exception err){ throw err;}
	throw Token::exception("Inverted List Construction");
	}
InvertedListTerm::~InvertedListTerm(){


	}

VirtualInvertedListTerm::VirtualInvertedListTerm(vector<Token*> TV, const string& ss):
	Term(ss){
  		for(int i=0; i<TV.size( ); i++);
			//Application.push_back(TV[i]);

		}



